fix(spl): align test_process_mint_to_checked's assumption to p-token#147
fix(spl): align test_process_mint_to_checked's assumption to p-token#147
Conversation
dkcumming
left a comment
dkcumming
left a comment
There was a problem hiding this comment.
I think this misses the mark. This does not match the p-token specification, it is similar but it is not the same. Our definition of equivalence is that we are using the same specification (with strictly necessary adjustments to account for the difference in the types included) to prove both implementations. Either the p-token harness needs to be changed to be same, or this should be changed to be the same as p-token. Realistically we should be able to diff the two postconditions and the only changes are because of the difference in the types.
I love this idea. Let me align these two specs and try me best to make the diff to be minimal. If you think it is good, I can present another pr for all the other specs. |
Stevengre
force-pushed
the
jh/fix_mint_to_checked_remote
branch
from
751e821 to
c9c0883
Compare
Stevengre
force-pushed
the
jh/fix_mint_to_checked_remote
branch
from
a77406d to
5352304
Compare
|
Maybe we can close this and use #150 directly. |
2 participants
No description provided.